;; The first four lines of this file were added by Dracula.
;; They tell DrScheme that this is a Dracula Modular ACL2 program.
;; Leave these lines unchanged so that DrScheme can properly load this file.
#reader(planet "reader.rkt" ("cce" "dracula.plt") "modular" "lang")
(require "mcolorshift.lisp")
(require "mbmptree.lisp")
(require "mavltree.lisp")


(module Tcolorshift
  (import Icolorshift)
  (import Ibmptree)
  (import Iavltree)
  
  (include-book "doublecheck" :dir :teachpacks) 
  (include-book "testing" :dir :teachpacks)
  
  (defrandom random-pixel ()
    (let* ((r (random-between 0 255))
           (g (random-between 0 255))
           (b (random-between 0 255)))
      (list r g b)))
  
  (defun fill-bitmap (tr xcurr ycurr height width pixels)
    (if (< xcurr height)
        ; yes, is the current y index less than its max?
        (if (< ycurr width)
            ; yes, put in random pixel
            (fill-bitmap (insert-pixel tr (list xcurr ycurr (car pixels))) xcurr (+ ycurr 1) height width (cdr pixels))
            ; no, so reset y to 0 and increment x
            (fill-bitmap tr (+ xcurr 1) 0 height width pixels))
        ; x has extended past its max, so the recursion is done - return the new tree
        tr))
  
  (defrandom random-bitmap ()
    (let* ((header (list 66 77 54 12 0 0 0 0 0 0 54 0 0 
                         0 40 0 0 0 25 0 0 0 25 0 0 0 1 
                         0 24 0 0 0 0 0 0 12 0 0 0 0 0 
                         0 0 0 0 0 0 0 0 0 0 0 0 0))
           (width 25)
           (height 25)
           (pixels (random-list-of (random-pixel) :size (* width height)))
           (tr (insert-header (empty-tree) header)))
      (fill-bitmap tr 0 0 height width pixels)))
  
  (check-expect (shift-pixel '(0 0 0) '(255 255 255) 0 0 0) '(255 255 255))
  (check-expect (shift-pixel '(0 0 0) '(255 255 255) 10 10 10) '(10 10 10))
  (check-expect (shift-pixel '(0 0 0) '(255 255 255) 0 0 10) '(0 0 10))
  (check-expect (shift-pixel '(0 0 0) '(255 255 255) 0 10 0) '(0 10 0))
  (check-expect (shift-pixel '(0 0 0) '(255 255 255) 10 0 0) '(10 0 0))
  (check-expect (shift-pixel '(0 0 0) '(255 255 255) 10 10 0) '(10 10 0))
  (check-expect (shift-pixel '(0 0 0) '(255 255 255) 0 10 10) '(0 10 10))
  (check-expect (shift-pixel '(0 0 0) '(255 255 255) 10 0 10) '(10 0 10))
  
  (defproperty shift-pixel-returns-list-prp
    (color :value (random-list-of (random-between 0 255))
            newcolor :value (random-list-of (random-between 0 255))
     r :value (random-between 0 255)
     g :value (random-between 0 255)
     b :value (random-between 0 255))
    (equal t (listp (shift-pixel color newcolor r g b))))
  
  (defproperty shift-pixel-returns-list-length-3 
    (color :value (random-list-of (random-between 0 255))
           newcolor :value (random-list-of (random-between 0 155))
           r :value (random-between 0 255)
           g :value (random-between 0 255)
           b :value (random-between 0 255))
    (equal 3 (length (shift-pixel color newcolor r g b))))
  
  (defproperty color-shift-helper-returns-tree
    (tr :value (random-bitmap)
        color :value (random-list-of (random-between 0 255))
        newcolor :value (random-list-of (random-between 0 255)))
    (equal t (tree? (color-shift-helper tr color newcolor 0 25 0 25))))
  
  (defproperty color-shift-returns-tree
    (tr :value (random-bitmap)
        color :value (random-list-of (random-between 0 255))
        newcolor :value (random-list-of (random-between 0 255)))
    (equal t (tree? (color-shift tr color newcolor))))
        
  
  )
(link RTcolorshift (Mavltree Mbmptree Mcolorshift Tcolorshift))
(invoke RTcolorshift)